(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun o () Int)
(declare-fun p () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun k () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(assert (<= 0 b 1))
(assert (< (- 2) o))
(assert (> (* g (abs (- 1 (- k c)))) (- (+ g (div (- c) (+ (* 2 h) (* k i) (* g j) 1)) 1) h) (+ k (* b n) (* b m)) (+ g (* o n) (* (+ (div b d) a) l) m) 0))
(assert (>= e 0))
(assert (> (+ (* k e) (* g f)) 0))
(assert (= (+ (* b e) (* o f)) 0))
(check-sat)
